-----------------------------------------------------------------------------
--
-- Module      :  Data.TypeLevel.Numbers
-- Copyright   :
-- License     :  AllRightsReserved
--
-- Maintainer  :  eduard.sergeev@gmail.com
-- Stability   :  Highly Experimental
-- Portability :
--
-- Type-level effective numbers
--
-----------------------------------------------------------------------------

{-# LANGUAGE NoImplicitPrelude, TypeFamilies, TypeOperators, UndecidableInstances,
ScopedTypeVariables, FlexibleInstances #-}


module Data.TypeLevel.Numbers (

   BInteger,

   (:==:),
   (:<=:),

--   (:::),
--   Nil,

   Succ,

   Zero,
   One,
   Two,
   Three,
   Four,
   Five,

) where

import Prelude (Show(show), Num(..))

import Data.TypeLevel.Class
import Data.TypeLevel.Families
import Data.TypeLevel.Bit
import Data.TypeLevel.Boolean
import qualified Data.TypeLevel.Peano as P
import Data.TypeLevel.List

data BInteger ds

-- * Type-level "Eq" implementation 
type instance BInteger lds :==: BInteger rds = (lds :==: rds) 


-- * Type-level "Ord" implementation 
type instance BInteger lds :<=: BInteger rds = Conv (Compare' lds rds)
type family Conv r :: *
type instance Conv GT = False
type instance Conv EQ = True
type instance Conv LT = True


type family Compare' l r :: *
type instance Compare' Nil Nil = EQ
type instance Compare' (lx ::: lxs) Nil = GT
type instance Compare' Nil (rx ::: rxs) = LT
type instance Compare' (lx ::: lxs) (rx ::: rxs) = Comb' (Compare lx rx) (Compare' lxs rxs)

type family Comb' l r :: *
type instance Comb' r LT = LT
type instance Comb' r GT = GT
type instance Comb' r EQ = r

type Zero = BInteger Nil
type One = BInteger (B1 ::: Nil)
type Two = BInteger (B0 ::: B1 ::: Nil)
type Three = BInteger (B1 ::: B1 ::: Nil)
type Four = BInteger (B0 ::: B0 ::: B1 ::: Nil)
type Five = BInteger (B1 ::: B0 ::: B1 ::: Nil)


-- Type-level "Num" implementation
--type instance BInteger lds :+: BInteger rds = 

instance (Numerable x, Numerable xs) => Numerable (x ::: xs) where
    toNumber _ = toNumber (typeValue :: x) + 2*(toNumber (typeValue :: xs))

instance Numerable Nil where
    toNumber _ = 0


instance (Numerable l) => Numerable (BInteger l) where
    toNumber _ = toNumber (typeValue :: l)

instance (Numerable l) => Show (BInteger l) where
    show n = show (toNumber n)


type family Succ n :: *
type instance Succ (BInteger ds) = BInteger (Succ ds)
type instance Succ Nil = (B1 ::: Nil)
type instance Succ (B0 ::: xs) = (B1 ::: xs)
type instance Succ (B1 ::: xs) = (B0 ::: (Succ xs))


t0 = typeValue :: Zero
t1 = typeValue :: One
t2 = typeValue :: Two
t3 = typeValue :: Three
t4 = typeValue :: Four
t5 = typeValue :: Five